2.5 Definitions and References

A function expression is a variable followed by a parameter list; a variable expression is a variable that is not followed by a parameter list. Function and variable expressions appear both in definitions and as subexpressions of larger expressions. The two usages are called definition and reference. References must be associated with definitions before they can be substituted or evaluated. This association, achieved through a process called binding, is discussed in §9.2 with an introduction in §2.5.1.

Figure 2.27 Formal (variable and function)

A parameter list is a comma-separated list of expressions in parenthesis. Parameters display as subscripts: f(x)+g(x,y) displays as f(x)+g(x, y). The terms formal and actual are used to distinguish defining and referencing occurrences of parameters and parameter lists. A parameter participating in a function definition is called a formal parameter in a formal parameter list. Formal parameters are constrained to be formal variables and functions (Figure 2.27).

Figure 2.28 Reference (variable and function)

The terms actual parameter and actual parameter list are used when referring to expressions participating in a reference (Figure 2.28). An actual parameter is sometimes called an argument. The second form of parameter list allows a tuple expression to be used in place of an actual parameter list.

A definition expression associates a formal definition with another expression called an elaboration. The syntax uses a binary “defines” operator. f(x)→x^2-1 defines a function and c→3⋅ℼ defines a variable. f(g(x), t)→g(t+1) defines a function with a function as a formal parameter. vʋ(aʋ, x)→aʋ+x (entered as vʋ(aʋ,x)→aʋ+x) defines a function that is parameterized by a vector and a real and produces a vector result.

2.5.1 Binding

Figure 2.29 Bindings for f(x)→g(x)+x^2+w, g(x)→(3⋅x)^3 and w→1

References – functions or variables that appear in an expression (2.28)– can be bound to definitions. References in an elaboration are bound to either formal parameters or non-local definitions. Figure 2.29 illustrates each sort of binding.

A function reference is bound to a function definition so the actual parameter values can be used in place of the formal parameters. A bound function reference can be transformed using either substitution or evaluation. Figure 2.30 shows two function references to the same function from the expression f(3⋅ℼ)+f(w÷2). Evaluated as two separate function activations, the argument 3⋅ℼ is used by the formal parameter x in one of the activations, and the argument w÷2 is used in the other. Transformed via substitution (twice), the expression becomes (3⋅ℼ)^2+w+((w÷2)^2+w). Transformed via evaluation, the expression is approximately 91.1. The example shows two references to f because it then becomes clear why the formal parameter is not shown as bound to the actual parameter; it would have to be bound to both actuals and this is not possible at the same moment in time. It is important to understand the meaning of the term “separate activations”. In fact, the binding of a formal parameter to a value is delayed until activation time.

2.5.1.1 Deferred Binding

Figure 2.31 Equivalent function references

Figure 2.28 (b) shows two forms of parameter list called the usual form and the deferred form. Figure 2.31 shows both forms used in equivalent expressions. The deferred form can be transformed into the usual form using special simplification.

Figure 2.32 Equivalent function references

Variations on the expressions in 2.31 are given in Figure 2.32. Example (a) shows a real variable concatenated with a tuple variable. Example (b) shows two variables, one a real and the other a tuple, bound to definitions and concatenated together.

The deferred form is used when parameters are assembled from a tuple expression, such as might occur when another function returns a tuple that must be “flattened” into the usual form of parameter list. That is, if uʈ→(3, 9) is to be bound to f(a, b)→a+b, the usual form would require the reference f(uʈ[0]., uʈ[1].). If uʈ was the result of another function, say uʈ→gʈ(3) where gʈ(x)→(x, x^2), the usual form would require f(gʈ(x)[0]., gʈ(x[1].)) which invokes gʈ(x) twice. The deferred form would be simply f←gʈ(3). However, the right-side of this expression must be evaluated before binding to f(a, b) can proceed.

To elaborate, binding succeeds when the signature of a reference matches the signature of a definition. Note the difference between f(x‖tʈ) and f←(x‖tʈ). The former binds to a function f(yʈ) while the latter binds to functions whose signature is not known until x‖tʈ has been evaluated to a tuple value so that the number of parameters and the type of each are known. Continuing with the previous example, f←gʈ(3) cannot be bound, and hence cannot be evaluated, until the signature of f is known. This can only happen when gʈ(3) is evaluated to produce a tuple value with known cardinality and element types.

2.5.1.2 Function parameters

Figure 2.33 Function parameter using lambda definition

An argument that is itself a function can be passed to a formal parameter that is itself a function formal. Such an argument can be represented by a lambda definition. Informally, a lambda definition is just an unnamed function. Its notation is that of a function definition with the symbol λ in place of the function name. Lambda definitions are discussed in §9.6. Figure 2.33 shows the bindings for a function parameter. Note there are three different functions named f, distinguished by the nature of their parameter lists. Computer scientists call this “overloading”.

2.5.2 Parameter inference

By its nature, a tablet computer with its soft keyboard makes expression input tedious. An alternative syntactic form of function definition that makes input easier uses parameter inference. For a left side with no explicit parameter list, as in f→x^2-1, the parameters are inferred from the expression on the right. Any number of definition parameters can be inferred: f→a+b+c infers three parameters and displays as f(a, b, c)→a+b+c.

The result type of a function definition with inferred parameters is itself inferred from the type of the elaboration. f→x infers f(x)→x and g→xⅈ infers gⅈ(xⅈ)→xⅈ. If the result type is provided explicitly, it suppresses inference and must match the type of the elaboration.

Parameter inference is performed in the parser. When the expression appears in the output area, inferred parameters will be present.

Sometimes variables in an elaboration are not local to the expression. That is, they are not associated with a formal parameter but rather with some other definition in the workspace. In this case, a formal parameter list must be provided and the variable is simply left out of the list.

When inference is too enthusiastic, the parameter list can be inferred for the active expression and then altered by selecting parameters individually and deleting them using . For example, two parameters are inferred for f(a, b)→a+b but if b is intended to be non-local, the parameter b in the active expression can be selected and removed to produce f(a)→a+b. With the definition b→2 elsewhere in the workspace, an expression like f(2) can be evaluated, transformed to 4. When the last parameter is removed, the function definition reverts to a variable definition.

Parameter inference can by suppressed by supplying an explicit parameter list or an explicit result type. Binding assumes any variable in the elaboration that does not appear in the parameter list is assumed to be non-local. But if all the variables in the elaboration are intended to be non-local, parameter inference would have to be suppressed by supplying an empty parameter list. Since parameterless functions can be confused with variables, inference can also be suppressed by providing a typed variable in the definition. That is, f.$-a+b suppresses inference to define a variable definition of f in terms of a and b.

2.5.3 Lambda inference

An expression that is not a definition and that is followed by a parameter list is promoted to a lambda definition by inference. That is, (x^2)(3) is promoted to (λx→x^2)(3) and displays as (λ(x)→x^2)(3). When simplified, the formal parameter x is bound to the actual parameter 3.

A lambda expression can also be inferred from an expression with more than one variable. The set of inferred variables implied by the expression is ordered alphabetically to produce the actual parameter list. Promotion of (x÷y)(1,2) produces (λ(x,y)→x÷y)(1,2). The ordering can sometimes be counter-intuitive. The very similar promotion of (x÷w)(1,2) produces (λ(w,x)→x÷w)(1,2) which would produce a different result.